COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	Pat Hayes, in his 1973 paper "Computation and Deduction", claimed that
C00011 ENDMK
C⊗;
Pat Hayes, in his 1973 paper "Computation and Deduction", claimed that
computation is "controlled deduction.  An interpreter for a programming
language is structurally indistinguishable from a theorem proving program
for a logical language.

He claimed that we could benfit greatly from the separation of the logic
and control components of a program, even  to the extent of having a
separate language for each.

The logic describes WHAT is to be computed, while the control specifies HOW.
Kowalski expanded on this theme in his 1976 paper "Algorithm = Logic + Control".
He divided up the logic and control components further according to this
diagram:




to prove the partial correctnss of an algorithm, one need only be concerned with
the logic component.   One can improve the efficiency by changing the control
component of a program without worrying about destroying its corectness (partial).
of course, termination is a control issue.


It is our thesis that at least the logic component of programs is language-independent.
Most programming languages at best, mix logic and control issues, and some may
even be considered as strictly control languages, the logic being a by-product
of actions taken.

Attempts at verification of complex programs have not been very successful.  We
feel that part of the problem is the attempt to derive the logic from the control
of the program.  Specifications (verification conditions) are added after the
program is already written.  Thus "specifications" is a mis-nomer.

By definition specifications should be writen before a program to accomplish the
goal described in the specs.  Correctness is the problem that is paramount in
programming, not efficiency.



Even the control issues mentioned in kowalski's diagram are language independent.


We have implemented a system which accepts specifications of the logic of programs
and some specification of control, generates algorithms in an intermediate
language, and then translates these algorithms into taret language programs.



The specification of an algorithm involves the following:




slide:  function specs:
		function name
		input pattern
		formal parameters
		precondition
		postcondition
		horn clauses

explain each then do gcd
	input pattern- tells which vars are input and which are output

although the functions we define may be read as relations, we insist that
the functions being defined are functions in that there is one unique answer
to every query or function call. that is, given a function with 4 parameters,
2 input and 2 output, there is exactly one tuple (x1 x2 x3 x4) for each
pair of input values, x1 and x2.


pre and post- specify functionality


Horn-clauses-  declarative and procedural semantics

	we differ from logic programming in the requirement for functionality,
which was not thought to be too restrictive considering the goal of generating
programs in existing target languages.

do gcd as example

		type specifications
		type name
		horn clauses

do exp example:  mention invertibility

generic specs


semantics of input as first-order logic statement


intermediate language:

syntax:  body of a function is a bktrkcond
		check precondition
		try alternatives in order


Mapping from input to intermediate
	do general function def then gcd
	do general generic def then exp
		explain how specific versions get substituted in

correctness of mapping
	indicate why ordering does not hurt

Mapping to target:

		slide showing general recipe

		slide showing mapping to lisp

		discussion of philosophy of implementation and its
efects on the kind of specifications allowed-- discuss both lisp implementations

discuss the use of undefined on both levels

discuss the use of output vars for negation
		do member
		do something which returns undef as answer

discuss or show correctness of the mapping to lisp

discuss problems foreseen with the pascal implementation and their implications


Correctness of specifications
		prove each horn clause as theorem of problem domain
		prove that the precondition guarantees termination
		prove that the program really guarantes the postcondition

Further work suggested by the system:
		front end to allow more natural input
			embedded function applications
			as well as less restricted use of logic
			from which the system could derive the specifications
			(including the Horn clauses) ala manna-waldinger/darlington
	extension of the use of generic functions to be selected 
		by type considerations as well as by input pattern;
	efficiency considerations: 
		specification and synthesis of an optimizer (transformation system)
			for a target language; 
	feasibility study of a system that could synthesize the "back end" 
		of the system automatically from a formal specification
		of the syntax and semantics of the target language; 
	inclusion of a way of specifying that "all" answers to a query 
		(or all elements of a relation) are desired.

		

SUMMARY:

		the natural way to achieve correct programs is to specify them
	in a high level language which is concerned only with correctness, contol
	issues can be considered separately.


		the specifications can be proven correct


		this approach is target language independent

		the system is "practical"- several sample programs have been 
			generated including a program synthesis system.